r:rationals. ((qeq(r; 0)))  (qinv(r)  rationals) 

latex

Definitions	qeq(r; s), P  Q, P  Q, P  Q, A, nequal(T; a; b), ff, if b then t else f fi , qinv(r), tt, int_nzero, b-union(A; B), rationals, t  T, P  Q, x:A. B(x), trans(T; x,y.E(x;y)), equiv_rel(T; x,y.E(x;y)), False, prop{i:l}, , subtype(S; T)
Lemmas	int inc rationals, qeq-wf, not wf, assert of eq int, eq int wf, qeq-equiv, assert wf, eqtt to assert, nequal wf, neg assert of eq int, int nzero wf, ifthenelse wf, bfalse wf, btrue wf, qeq wf, bool wf, rationals wf